(set-logic QF_UFBV)
(declare-fun _substvar_31_ () Bool)
(declare-sort S0 0)
(declare-const S0-0 S0)
(declare-const S0-2 S0)
(declare-const bv_1-0 (_ BitVec 1))
(assert (= true true true _substvar_31_ true true (= S0-0 S0-2 S0-0) true true true (distinct (_ bv0 1) bv_1-0)))
(check-sat)
